﻿module CSValidation
open CSModel
type ExprType = Symbol | Numeric | Bool

exception NotInDomain of (Def*Val)
exception EmptyDomain of Def
exception DomainMismatch of (Def*Val)
exception NotBoolExpression of Expr
exception TypeMismatch of ExprType*ExprType
exception DuplicateVariable of string
exception NoVariableReferencedInExpression

let isInDomain (VarDef(n,d)) (v:Val) = 
    match d,v with
    | Di xs, ValI x -> ()
    | Ds xs, ValS s -> if xs|>Seq.exists (fun x->x=s) then () else (VarDef(n,d),v)|>NotInDomain|>raise
    | _,_ -> (VarDef(n,d),v) |> DomainMismatch |> raise
let valType=function ValS _ ->ExprType.Symbol|_->ExprType.Numeric
let validateVariableNames (xs:seq<Def>) =
    let a,b = 
        xs
        |>Seq.map (function VarDef(n,_)->n) 
        |> Seq.countBy (fun x->x) 
        |> Seq.maxBy(fun (k,v)->v)
    if b > 1 then DuplicateVariable(a)|>raise
let validateDomain (VarDef(n,d)) = 
    match d with 
    | Di s -> if Seq.isEmpty s then VarDef(n,d)|>EmptyDomain|>raise
    | Ds s -> if Seq.isEmpty s then VarDef(n,d)|>EmptyDomain|>raise

let typeExpr expr = 
    match expr with
    | Eq (_,_)  | Neq (_,_) | Not _ 
    | Neq (_,_) | And _     | Or _ -> ExprType.Bool
    | Div (_,_)  | Mult (_,_)  | Abs(_)
    | Plus (_,_) | Minus (_,_) | Mod (_,_) 
    | Ge (_,_)   | Gt(_,_)     | Le(_,_) 
    | Lt(_,_) -> ExprType.Numeric
    | Var (VarDef(_,d)) -> match d with Di _ -> ExprType.Numeric | Ds _ -> ExprType.Symbol
    | Val a-> a|>valType

let validateNumeric(e1:Expr,e2:Expr) = 
    let te1 = typeExpr e1
    let te2 = typeExpr e2
    if te1 = ExprType.Numeric && te2 = ExprType.Numeric then ()
    else raise (TypeMismatch(te1,te2))

let scope expr =
    let rec loop acc e =
        match e with
        | Var v -> v::acc
        | Val _ -> acc
        | Plus (a,b) | Minus (a,b) | Div (a,b)  | Eq (a,b) 
        | Mod (a,b)  | Mult(a,b)   | Ge (a,b)   | Gt (a,b) 
        | Lt (a,b)   | Le(a,b)     
        | Neq (a,b) ->  loop (loop acc a) b
        | And xs | Or xs -> xs |> Seq.fold loop acc
        | Abs x  | Not x -> loop acc x
    let vs = loop [] expr
    vs
    
let rec validateExpression exp =
    match exp with
    | Val _ -> ()
    | Var v -> validateDomain v
    | Eq (Var var, Val v) -> isInDomain var v; validateExpression (Var var)
    | Eq (Val v, Var var) -> isInDomain var v; validateExpression (Var var)
    | Eq (e1,e2) -> 
        validateExpression e1
        validateExpression e2
        let te1 = typeExpr e1 
        let te2 = typeExpr e2
        if te1<>te2 then raise (TypeMismatch(te1,te2))
    | Neq (Var var, Val v) -> isInDomain var v; validateExpression (Var var)
    | Neq (Val v, Var var) -> isInDomain var v; validateExpression (Var var)
    | Neq (e1,e2) -> 
        validateExpression e1
        validateExpression e2
        let te1 = typeExpr e1 
        let te2 = typeExpr e2
        if te1<>te2 then raise (TypeMismatch(te1,te2))
    | And xs->xs|>Seq.iter validateExpression
    | Or xs->xs|>Seq.iter validateExpression
    | Not x -> validateExpression x
    | Div (e1,e2) | Minus (e1,e2) | Mod (e1,e2) | Mult (e1,e2)
    | Ge (e1,e2)  | Gt (e1,e2)    | Le (e1,e2)  | Lt (e1,e2) 
    | Plus (e1,e2) -> validateExpression e1; validateExpression e2; validateNumeric (e1,e2)
    | Abs (e1) -> validateExpression e1; validateNumeric(e1,e1)

let validate (ConstraintSystem(vars,exprs)) =
    vars  |> validateVariableNames
    vars  |> Seq.iter validateDomain
    exprs |> Seq.iter validateExpression
    exprs |> Seq.map scope |> Seq.iter (fun s -> if s |> Seq.isEmpty then raise NoVariableReferencedInExpression)
